1. Technical Field
The present invention relates to computer verification and more particularly to decomposing bounded model checking to improve efficiency and reduce complexity for computer program verification.
2. Description of the Related Art
Bounded Model Checking (BMC) is a technique used in computer program verification. BMC provides complete design coverage with respect to a correctness property for a bounded depth. In spite of using richer expressive theories to obtain compact representation, and using on-the-fly circuit simplification, each BMC instance at depth k grows bigger in size and harder to solve with successive unrolling of the design. To build a scalable framework, it is quite imperative to decompose each BMC problem at depth k into smaller sub-problems that can be solved separately to reduce the peak resource requirement.
Moreover, to efficiently exploit modern servers with many-core CPUs, it is important that these sub-problems be solved independently with minimum sharing of information. Further, due to memory limitations of single servers, it is important that these sub-problems also have small memory footprints.
Several techniques for decomposition symbolic traversal techniques have been employed to address these issues. However, these symbolic traversal techniques do not address the scalability requirement. In BDD-based approaches in the art, the transition relation and reachable state space are partitioned, and disjunctive image computations are carried out on each partition independently. Such a state-based partitioning approach requires “remembering” the reachable states explored by each sub-problem.
Though, these methods avoid intermediate blow-up of image computation, re-partitioning of reachable states for a next traversal step can be quite resource intensive. When implemented in a distributed environment or on a many-core CPU server, such an approach will incur large communication costs in redistributing the results of disjunctive image operations.
In a distributed BMC approach, each BMC instance is partitioned structurally so that each processor gets an exclusive number of consecutive BMC time frames. The distributed problem is then solved by a distributed SAT, managed by a central server. Though this method overcomes the memory limitation of single processor, and employs fine grain parallelization of Boolean or propositional satisifiability (SAT), it incurs significant communication overhead during exchange of lemmas and propagation of values across partition interfaces, especially, when the BMC instance is difficult to solve.
In another BMC approach, the partitioning of a BMC instance is performed over conjunction and disjunction of property sub-formulas so as to exploit incremental learning. However, for an atomic sub-formula the BMC instance is not partitioned further.
In a sequential ATPG-based approach, explicit state traversal and unrollings are avoided; rather, solution state cubes at each time frame are enumerated, either in a depth or breath first manner, and which need to be justified. Since the state space is typically exponential for real-world design, this method can potentially space out, in spite of various state caching and pruning techniques proposed for storing solution state cubes. Moreover, this method does not guarantee a shortest counter-example if one exists. This method suffers from the same problem as state-based partitioning approaches.
In symbolic execution used in testing, instead of breadth first symbolic traversal, depth first symbolic traversal is made for a bounded depth. Path conditions are generated for the chosen program path to constrain the symbolic path. Such a method can be considered as an extreme case of partitioning where each program path is explored separately. Completeness for bounded depth is guaranteed by exploring all program paths separately. Since there could be multiple program paths (cross product of each branching condition), such an approach has large overhead.
In an abstraction refinement based approach, each abstract path chosen is a program path with incomplete path conditions. In each refinement step (using a constraint solver), path conditions are derived that are either necessary for showing a concrete witness or are sufficient to show no witness.